/* memcpy */
/* Variables: n */

/* Program: */
/* local s1, s2 { */
/* src := malloc(s1); */
/* dst := malloc(s2); */
/* assert n <= s2 && n <= s1; */
/* assert 1 <= s2 && 1 <= s1; */
/* }; */
/* local i { */
/* i := 0; */
/* while i < n do */
/*   dst[i] := src[i]; */
/*   i := i+1; */
/* done; */
/* }; */


void mymemcpy(int n, int s1, int s2){
  char *src = malloc(s1);
  char *dst = malloc(s2);

  assert((n <= s2) && (n <= s1));
  
  assert((1 <= s2) && (1 <= s1));

  int i = 0;
  while (i < n){
    dst[i] = src[i];
    i = i + 1;
  }
  printf("n s d\n");
  printf("%d %d %d\n",n,(unsigned)strlen(src),(unsigned)strlen(dst));
}


/* strncpy */
/* Variables: n */

/* Program: */
/* local s1, s2 { */
/* src := malloc(s1); */
/* dst := malloc(s2); */
/* assert 0 <= s1 && n <= s1; */
/* assert 0 <= s2 && n <= s2; */
/* }; */
/* local i { */
/* i := 0; */
/* while i < n && src[i] != '\0' do */
/*   dst[i] := src[i]; */
/*   i := i+1; */
/* done; */
/* while i < n do */
/*   dst[i] := '\0'; */
/*   i := i+1; */
/* done; */
/* }; */



/*partial_decr0*/
/* Variables: i, n */

/* Program: */
/* i = 0; */
/* while i > n do */
/*   i = i-1; */
/* done; */


void par_decr0(int n){

  int i = 0;
  while (i > n){
    i = i - 1;
  }
  //inv

  printf ("i n\n");
  printf("%d %d\n",i,n);

}


void par_incr0(int n){

  int i = 0;
  while (i <= n){
    i = i + 1;
  }
  //inv

  printf ("i n\n");
  printf("%d %d\n",i,n);

}


/*partial_decr1*/
/* Variables: i, p, q */

/* Program: */
/* i = p; */
/* while i > q do */
/*   i = i-1; */
/* done; */

void par_decr1(int p, int q){

  int i = p;
  while (i > q){
    i = i - 1;
  }
  //inv
  assert(i==min(p,q));
  printf ("i p q\n");
  printf("%d %d %d\n",i,p,q);

}


void par_incr1(int p, int q){

  int i = p;
  while (i < q){
    i = i + 1;
  }
  //inv
  assert(i==max(p,q));
  printf ("i p q\n");
  printf("%d %d %d\n",i,p,q);

}




/* partial_decr2 */
/* Variables: i, p, q, r */

/* Program: */
/* i = p; */
/* while i > q do */
/*   i = i-1; */
/* done; */
/* while i > r do */
/*   i = i-1; */
/* done; */


void par_decr2(int p, int q, int r){

  int i = p;
  while (i > q){
    i = i - 1;
  }

  while (i > r){
    i = i - 1;
  }

  //inv
  assert(i==min(min(p,q),r));
  printf ("i p q r\n");
  printf("%d %d %d %d\n",i,p,q,r);

}


void par_incr2(int p, int q, int r){

  int i = p;
  while (i < q){
    i = i + 1;
  }

  while (i < r){
    i = i + 1;
  }
  //inv
  assert(i==max(max(p,q),r));
  printf ("i p q r\n");
  printf("%d %d %d %d\n",i,p,q,r);

}



/* partial_decr3 */
/* Variables: i, p, q, r, s */

/* Program: */
/* i = p; */
/* while i > q do */
/*   i = i-1; */
/* done; */
/* while i > r do */
/*   i = i-1; */
/* done; */
/* while i > s do */
/*   i = i-1; */
/* done; */

void par_decr3(int p, int q, int r, int s){

  int i = p;
  while (i > q){
    i = i - 1;
  }

  while (i > r){
    i = i - 1;
  }

  while (i > s){
    i = i - 1;
  }

  //inv
  assert(i==min(min(min(p,q),r),s));
  printf ("i p q s\n");
  printf("%d %d %d %d %d\n",i,p,q,r,s);

}


void par_incr3(int p, int q, int r, int s){

  int i = p;
  while (i < q){
    i = i + 1;
  }

  while (i < r){
    i = i + 1;
  }

  while (i < s){
    i = i + 1;
  }

  //inv
  assert(i==max(max(max(p,q),r),s));
  printf ("i p q s\n");
  printf("%d %d %d %d %d\n",i,p,q,r,s);

}


/* partial_decr4 */
/* Variables: i, p, q, r, s, t */

/* Program: */
/* i = p; */
/* while i > q do */
/*   i = i-1; */
/* done; */
/* while i > r do */
/*   i = i-1; */
/* done; */
/* while i > s do */
/*   i = i-1; */
/* done; */
/* while i > t do */
/*   i = i-1; */
/* done; */

void par_decr4(int p, int q, int r, int s, int t){

  int i = p;
  while (i > q){
    i = i - 1;
  }

  while (i > r){
    i = i - 1;
  }

  while (i > s){
    i = i - 1;
  }

  while (i > t){
    i = i - 1;
  }


  //inv
  assert(i==min(min(min(min(p,q),r),s),t));
  printf ("i p q s t\n");
  printf("%d %d %d %d %d %d\n",i,p,q,r,s,t);

}


void par_incr4(int p, int q, int r, int s, int t){

  int i = p;
  while (i < q){
    i = i + 1;
  }

  while (i < r){
    i = i + 1;
  }

  while (i < s){
    i = i + 1;
  }

  while (i < t){
    i = i + 1;
  }

  //inv
  assert(i==max(max(max(max(p,q),r),s),t));
  printf ("i p q s t\n");
  printf("%d %d %d %d %d %d\n",i,p,q,r,s,t);

}

/* partial_decr5 */
/* Variables: i, p, q, r, s, t, u */

/* Program: */
/* i = p; */
/* while i > q do */
/*   i = i-1; */
/* done; */
/* while i > r do */
/*   i = i-1; */
/* done; */
/* while i > s do */
/*   i = i-1; */
/* done; */
/* while i > t do */
/*   i = i-1; */
/* done; */
/* while i > u do */
/*   i = i-1; */
/* done; */
void par_decr5(int p, int q, int r, int s, int t, int u){

  int i = p;
  while (i > q){
    i = i - 1;
  }

  while (i > r){
    i = i - 1;
  }

  while (i > s){
    i = i - 1;
  }

  while (i > t){
    i = i - 1;
  }

  while (i > t){
    i = i - 1;
  }

  while (i > u){
    i = i - 1;
  }


  //inv
  assert(i==min(min(min(min(min(p,q),r),s),t),u));
  printf ("i p q s t u\n");
  printf("%d %d %d %d %d %d %d\n",i,p,q,r,s,t,u);

}


void par_incr5(int p, int q, int r, int s, int t, int u){

  int i = p;
  while (i < q){
    i = i + 1;
  }

  while (i < r){
    i = i + 1;
  }

  while (i < s){
    i = i + 1;
  }

  while (i < t){
    i = i + 1;
  }

  while (i < u){
    i = i + 1;
  }

  //inv
  assert(i==max(max(max(max(max(p,q),r),s),t),u));
  printf ("i p q s t u\n");
  printf("%d %d %d %d %d %d %d\n",i,p,q,r,s,t,u);

}



void oddeven4(int t0, int t1, int t2, int t3){

  int x0 = t0;
  int x1 = t1;
  int x2 = t2;
  int x3 = t3;

  int u;
  if (x0 > x1){
      u = x0;
      x0 = x1;
      x1 = u;
    }

  if (x2 > x3){
    u = x2;
    x2 = x3;
    x3 = u;
  }

  if (x1 > x2){
    u = x1;
    x1 = x2;
    x2 = u;
  }

  if (x0 > x1){
    u = x0;
    x0 = x1;
    x1 = u;
  }
  
  if (x2 > x3){
    u = x2;
    x2 = x3;
    x3 = u;
  }

  if (x1 > x2){
    u = x1;
    x1 = x2;
    x2 = u;
  }

  assert (x0 <= x1 && x1 <= x2 && x2 <= x3);
  printf("x0 x1 x2 x3 t0 t1 t2 t3\n");
  printf("%d %d %d %d %d %d %d %d\n",x0,x1,x2,x3,t0,t1,t2,t3);
}


void oddeven5(int t0, int t1, int t2, int t3, int t4){
 
  int x0 = t0;
  int x1 = t1;
  int x2 = t2;
  int x3 = t3;
  int x4 = t4;

  int u;
  if (x0 > x1){
    u = x0;
    x0 = x1;
    x1 = u;
  }
  if (x2 > x3){
    u = x2;
    x2 = x3;
    x3 = u;
  }
  if (x1 > x2){
    u = x1;
    x1 = x2;
    x2 = u;
  }
  if (x3 > x4){
    u = x3;
    x3 = x4;
    x4 = u;
  }
  if (x0 > x1){
    u = x0;
    x0 = x1;
    x1 = u;
  }
  if (x2 > x3){
    u = x2;
    x2 = x3;
    x3 = u;
  }
  if (x1 > x2){
    u = x1;
    x1 = x2;
    x2 = u;
  }
  if (x3 > x4){
    u = x3;
    x3 = x4;
    x4 = u;
  }
  if (x0 > x1){
    u = x0;
    x0 = x1;
    x1 = u;
  }
  if (x2 > x3){
    u = x2;
    x2 = x3;
    x3 = u;
  }
  if (x1 > x2){
    u = x1;
    x1 = x2;
    x2 = u;
  }
  if (x3 > x4){
    u = x3;
    x3 = x4;
    x4 = u;
  }

  assert (x0 <= x1 && x1 <= x2 && x2 <= x3 && x3 <= x4);

  printf("x0 x1 x2 x3 x4\n");
  printf("%d %d %d %d %d\n",x0,x1,x2,x3,x4);

}

void oddeven6(int t0, int t1, int t2, int t3, int t4, int t5){

  int x0 = t0;
  int x1 = t1;
  int x2 = t2;
  int x3 = t3;
  int x4 = t4;
  int x5 = t5;
  int u;
 
  if (x0 > x1){
    u = x0;
    x0 = x1;
    x1 = u;
  }
  if (x2 > x3){
    u = x2;
    x2 = x3;
    x3 = u;
  }
  if (x4 > x5){
    u = x4;
    x4 = x5;
    x5 = u;
  }
  if (x1 > x2){
    u = x1;
    x1 = x2;
    x2 = u;
  }
  if (x3 > x4){
    u = x3;
    x3 = x4;
    x4 = u;
  }
  if (x0 > x1){
    u = x0;
    x0 = x1;
    x1 = u;
  }
  if (x2 > x3){
    u = x2;
    x2 = x3;
  x3 = u;
  }
  if (x4 > x5){
    u = x4;
    x4 = x5;
    x5 = u;
  }
  if (x1 > x2){
    u = x1;
    x1 = x2;
    x2 = u;
  }
  if (x3 > x4){
    u = x3;
    x3 = x4;
    x4 = u;
  }
  if (x0 > x1){
    u = x0;
    x0 = x1;
    x1 = u;
  }
  if (x2 > x3){
    u = x2;
    x2 = x3;
    x3 = u;
  }
  if (x4 > x5){
    u = x4;
    x4 = x5;
    x5 = u;
  }
  if (x1 > x2){
    u = x1;
    x1 = x2;
    x2 = u;
  }
  if (x3 > x4){
    u = x3;
    x3 = x4;
    x4 = u;
  }

  assert (x0 <= x1 && x1 <= x2 && x2 <= x3 && x3 <= x4 && x4 <= x5);

  printf("x0 x1 x2 x3 x4 x5 t0 t1 t2 t3 t4 t5\n");
  printf("%d %d %d %d %d %d %d %d %d %d %d %d\n",x0,x1,x2,x3,x4,x5,t0,t1,t2,t3,t4,t5);
}

void oddeven7(int t0, int t1, int t2, int t3, int t4, int t5, int t6){
  
  int x0 = t0;
  int x1 = t1;
  int x2 = t2;
  int x3 = t3;
  int x4 = t4;
  int x5 = t5;
  int x6 = t6;
  int u;
  if (x0 > x1){
    u = x0;
    x0 = x1;
    x1 = u;
  }
  if (x2 > x3){
    u = x2;
    x2 = x3;
    x3 = u;
  }
  if (x4 > x5){
    u = x4;
    x4 = x5;
    x5 = u;
  }
  if (x1 > x2){
    u = x1;
    x1 = x2;
    x2 = u;
  }
  if (x3 > x4){
    u = x3;
    x3 = x4;
    x4 = u;
  }
  if (x5 > x6){
    u = x5;
    x5 = x6;
    x6 = u;
  }
  if (x0 > x1){
    u = x0;
    x0 = x1;
    x1 = u;
 }
  if (x2 > x3){
    u = x2;
    x2 = x3;
    x3 = u;
  }
  if (x4 > x5){
    u = x4;
    x4 = x5;
    x5 = u;
  }
  if (x1 > x2){
    u = x1;
    x1 = x2;
    x2 = u;
  }
  if (x3 > x4){
    u = x3;
    x3 = x4;
    x4 = u;
  }
  if (x5 > x6){
    u = x5;
    x5 = x6;
    x6 = u;
  }
  if (x0 > x1){
    u = x0;
    x0 = x1;
    x1 = u;
  }
  if (x2 > x3){
    u = x2;
    x2 = x3;
    x3 = u;
  }
  if (x4 > x5){
    u = x4;
    x4 = x5;
    x5 = u;
  }
  if (x1 > x2){
    u = x1;
    x1 = x2;
    x2 = u;
  }
  if (x3 > x4){
    u = x3;
    x3 = x4;
    x4 = u;
  }
  if (x5 > x6){
    u = x5;
    x5 = x6;
    x6 = u;
  }
  if (x0 > x1){
    u = x0;
    x0 = x1;
    x1 = u;
  }
  if (x2 > x3){
    u = x2;
    x2 = x3;
    x3 = u;
  }
  if (x4 > x5){
    u = x4;
    x4 = x5;
    x5 = u;
  }
  if (x1 > x2){
    u = x1;
    x1 = x2;
    x2 = u;
  }
  if (x3 > x4){
    u = x3;
    x3 = x4;
    x4 = u;
  }
  if (x5 > x6){
    u = x5;
    x5 = x6;
    x6 = u;
  }

  assert (x0 <= x1 && x1 <= x2 && x2 <= x3 && x3 <= x4 && x4 <= x5 && x5 <= x6);

  printf("x0 x1 x2 x3 x4 x5 x6\n");
  printf("%d %d %d %d %d %d %d\n",x0,x1,x2,x3,x4,x5,x6);
}

void oddeven8(int t0, int t1, int t2, int t3, int t4, int t5, int t6, int t7){
  
  int x0 = t0;
  int x1 = t1;
  int x2 = t2;
  int x3 = t3;
  int x4 = t4;
  int x5 = t5;
  int x6 = t6;
  int x7 = t7;
  int u;
  if (x0 > x1){
    u = x0;
    x0 = x1;
    x1 = u;
  }
  if (x2 > x3){
    u = x2;
    x2 = x3;
    x3 = u;
  }
  if (x4 > x5){
    u = x4;
    x4 = x5;
    x5 = u;
  }
  if (x6 > x7){
    u = x6;
    x6 = x7;
    x7 = u;
  }
  if (x1 > x2){
    u = x1;
    x1 = x2;
    x2 = u;
  }
  if (x3 > x4){
    u = x3;
    x3 = x4;
    x4 = u;
  }
  if (x5 > x6){
    u = x5;
    x5 = x6;
    x6 = u;
  }
  if (x0 > x1){
    u = x0;
    x0 = x1;
    x1 = u;
  }
  if (x2 > x3){
    u = x2;
    x2 = x3;
    x3 = u;
  }
  if (x4 > x5){
    u = x4;
    x4 = x5;
    x5 = u;
  }
  if (x6 > x7){
    u = x6;
    x6 = x7;
    x7 = u;
  }
  if (x1 > x2){
    u = x1;
    x1 = x2;
    x2 = u;
  }
  if (x3 > x4){
    u = x3;
    x3 = x4;
    x4 = u;
  }
  if (x5 > x6){
    u = x5;
    x5 = x6;
    x6 = u;
  }
  if (x0 > x1){
    u = x0;
    x0 = x1;
    x1 = u;
  }
  if (x2 > x3){
    u = x2;
    x2 = x3;
    x3 = u;
  }
  if (x4 > x5){
    u = x4;
    x4 = x5;
    x5 = u;
  }
  if (x6 > x7){
    u = x6;
    x6 = x7;
    x7 = u;
  }
  if (x1 > x2){
    u = x1;
    x1 = x2;
    x2 = u;
  }
  if (x3 > x4){
    u = x3;
    x3 = x4;
    x4 = u;
  }
  if (x5 > x6){
    u = x5;
    x5 = x6;
    x6 = u;
  }
  if (x0 > x1){
    u = x0;
    x0 = x1;
    x1 = u;
  }
  if (x2 > x3){
    u = x2;
    x2 = x3;
    x3 = u;
  }
  if (x4 > x5){
    u = x4;
    x4 = x5;
    x5 = u;
  }
  if (x6 > x7){
    u = x6;
    x6 = x7;
    x7 = u;
  }
  if (x1 > x2){
    u = x1;
    x1 = x2;
    x2 = u;
  }
  if (x3 > x4){
    u = x3;
    x3 = x4;
    x4 = u;
  }
  if (x5 > x6){
    u = x5;
    x5 = x6;
    x6 = u;
  }

  assert (x0 <= x1 && x1 <= x2 && x2 <= x3 && 
	  x3 <= x4 && x4 <= x5 && x5 <= x6 && x6 <= x7);

  printf("x0 x1 x2 x3 x4 x5 x6 x7\n");
  printf("%d %d %d %d %d %d %d\n",x0,x1,x2,x3,x4,x5,x6,x7);
}






/*
  Examples from the paper InvGen: An Eﬃcient Invariant Generator by Ashutosh Gupta and Andrey Rybalchenko
  
 */

void fig2a(int n){
  int x = 0;
  printf("x n\n");
  while(1){
    printf("%d %d\n",x,n);
    if(!(x<n)){
      break;
    }
    x++;
  }
}



/*
  Examples from the paper Extending Dynamic Constraint Detection with Disjunctive
Constraints by Nadya Kuzmina, John Paul, Ruben Gamboa, and James Caldwell
 */

void calculator_numberpressed(int number){
  int displayValue = 100;
  if (number){
    displayValue = number ;
  }
  else{
    displayValue = displayValue * 10  + number ;
  }
}


void calculator_equals(int choice){
  int result = 0;
  if (choice == 1){
    result = result + 10;
  }
  else{
    result = 10 - result;
  }
}


/* From the thesis Disjunctive Invariants for Modular Static Analysis by 
Corneliu Popee

See page 7 more the complete example -- quite interesting if I can get all these invs

Lots more example from this guy's thesis -- very interesting ones too
 */

void fig1_1(int x){
  int y; int b;
  if (x > 0) {
    y = x;
  }
  else { 
    y = -x;
  }
  
  if (y>10){
    b = 1;
  }
  else{
    b = 0;
  }


  printf("x y b\n");
  printf("%d %d %d\n",x,y,b);

  //inv
  
  int c1 = (b == 1 && y > 10 && y == x) ;
  int c2 = (b == 1 && y > 10 && y == -x) ;
  int c3 = (b == 0 && y <= 10 && x > 0 && y == x) ;
  int c4 = (b == 0 && y <= 10 && x <= 0 && y == -x) ;
  assert(c1 || c2 || c3 || c4);

 

  assert ((x > 0 && y == x) || (x <= 0 && y == -x));

  //b => (x < -10 or 10 < x)
  assert (b==0 || (x < 10 || 10 < x));

  //I think this is also an inv
  //b = 0 =>  !(x < -10 || 10 < x)
  assert(b == 1 || (x >= -10 && 10 >= x));

  //in other words,  b *iff* (x <-10 || 10 < x)
}


int fig2_6_mn(int x){
  if (x > 0){
    x = fig2_6_mn(x-1);
  }
  
  return x;
}

void fig2_6_mn_caller(int x){
  int t = fig2_6_mn(x);
  //inv 

  printf("x t\n");
  printf("%d %d\n",x,t);
  assert ((x <= 0 && t==x) || (x > 0  && t==0));  
}



int f91(int x) {
  if (x<=100){
    return f91(f91(x+11));
  }
  else{
    return x-10;
  }
}

int f91_caller(int x){
  int t = f91(x);
  printf("x t\n");
  printf("%d %d\n",x,t);
  assert((x >= 101 && t==x-10) || (x<=100 && t == 91) );
}

// quicksort

void swap(float a[], int i, int j) {
  float temp = a[i]; 
  a[i] = a[j]; 
  a[j] = temp;
}


int changeN(float a[], int n, int i, int h, float v) { 
  if (i <= h){
    if (a[i] < v){ 
      swap(a,n+1,i); 
      return changeN(a,n+1,i+1,h,v);
    } 
    else { 
      return changeN(a,n,i+1,h,v);
    } 
  } 
  else { 
    return n ;
  } 
}

int mypartition(float a[], int l, int h){
  int v = a[l]; 
  int n = changeN(a,l,l+1,h,v); 
  swap(a,l,n);
  return n ;
}


/* MY EXAMPLES */

void maxfun(int a, int b, int c){
  int t = a ;
  if (b > t){
    t = b;
  }
  if (c > t){
    t = c;
  }
  printf("a b c t\n");
  printf("%d %d %d %d\n",a,b,c,t);
}


void myminmax(const int a, const int b){
  //suppose to give max(x,y) >= max(a,b)
  //similar to the mymemcpy but easier for me to debug

  int x = a;
  int y = b;
  
  int i = 0 ;
  printf("a b x y\n");
  while(i < 10){
    printf("%d %d %d %d\n",a,b,x,y);
    assert(max(x,y) >= max(a,b));

    if (x == max(x,y)){
      x = x + randrange_i(0,100,1);
      y = y + randrange_i(-100,100,1);
    }
    else{
      y = y + randrange_i(0,100,1);
      x = x + randrange_i(-100,100,1);
    }
    i++;
  }


}
